\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ \=($\forall$$e$, ${\it e'}$:E.\+
\\[0ex]($\uparrow$isrcv(kind($e$)))
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv(kind(${\it e'}$)))
\\[0ex]$\Rightarrow$ (lnk(kind($e$)) = lnk(kind(${\it e'}$)) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ \=($e$ $<$c ${\it e'}$\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(sender($e$) $<$c sender(${\it e'}$)\+
\\[0ex]$\vee$ (sender($e$) = sender(${\it e'}$) $\in$ E \& (index($e$) $<$ index(${\it e'}$))))))
\-\-\-
\end{tabbing}